飯田隆『言語哲学大全 I (旧版) 論理と言語』

単称名がないクワインの言語でも(自由)変項がその役割を果たす p.209

→コンビネータ計算を使うとどうなる? (言語哲学大全 IVの脚注にはコンビネータ計算が言及されている)

∀x. (ソクラテスる(x) ⇒ 死ぬ(x))

S(B(⇒)ソクラテスる)死ぬx

-> ((B(⇒)ソクラテスる)x)(死ぬx)

-> ((⇒)(ソクラテスるx))(死ぬx)

∀ (S(B(⇒)ソクラテスる) 死ぬ)

コンビネータ版についてどう推論規則を定めるか

コンビネータ論理は元来、本質的に量化変数を消去することによって量化変数の役割を明確にするような「pre-logic」を意図していた。量化変数を消去する方法にはクワインの述語関手論理がある。コンビネータ論理の表現力は一階述語論理を超える一方、述語関手論理の表現力は一階述語論理と同等である。